Nuprl Lemma : select_zip
4,23
postcript
pdf
T1
,
T2
:Type,
as
:
T1
List,
bs
:
T2
List,
i
:
.
i
<||zip(
as
;
bs
)||
zip(
as
;
bs
)[
i
] = <
as
[
i
],
bs
[
i
]>
T1
T2
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
zip(
as
;
bs
)
,
||
as
||
,
,
Prop
,
P
Q
,
False
,
A
,
A
B
,
{
T
}
,
SQType(
T
)
,
P
Q
,
Dec(
P
)
,
hd(
l
)
,
i
<
j
,
i
j
,
l
[
i
]
,
P
&
Q
,
P
Q
,
P
Q
Lemmas
zip
length
,
select
cons
tl
,
le
wf
,
decidable
int
equal
,
nat
wf
,
length
wf1
,
zip
wf
origin
T1, T2:Type, as:T1 List, bs:T2 List, i:
.
zip(as;bs)[i] = <as[i],bs[i]> 
T1
T2 T1, T2:Type, as:T1 List, bs:T2 List, i:.
zip(as;bs)[i] = <as[i],bs[i]> T1T2 Tx:A. B(x) Q
A
B
Q
jj
Q Q